es:ES, T:Type, I:MaInterface(T).
ma-interface-consistent2(es;I)  (Ia1,Ia2[[I|]].  Ia1  Ia2 = 0) 

latex

Definitions	P  Q, x:A. B(x), AbsInterface(A), [[I|]], X  Y = 0, (x,yL.  P(x;y)), ma-interface-consistent2(es;I), MaInterface(T), Type, ES, ma-interface-consistent(es;X), Id, (x  l), t  T, x:AB(x), [[I|i]], {x:A| B(x)} , x.A(x), P  Q, P & Q, P  Q, x,y. t(x;y), ma-interface-locs(I), remove-repeats(eq;L), False, A, left + right, P  Q, Dec(P), Atom$n, x:A  B(x), IdDeq, s = t, , no_repeats(T;l), E, b, Void, e  X
Lemmas	assert wf, es-is-interface wf, ma-interface-triggers-loc, es-E wf, remove-repeats property, no-repeats-pairwise, es-interface-disjoint wf, not wf, member-remove-repeats, decidable l member, decidable equal Id, pairwise-map2, ma-interface-triggers wf, ma-interface-consistent-consistent2